\begin{tabbing}
$\forall$$T$:(Id$\rightarrow$Type), ${\it tab}$:secret{-}table($T$).
\\[0ex]atoms{-}distinct(${\it tab}$)
\\[0ex]$\Rightarrow$ \=($\forall$$x$:Atom1, $n$:\{0..$\parallel$${\it tab}$$\parallel$ $^{-}$\}.\+
\\[0ex]($n$ $\leq$ ptr(${\it tab}$))
\\[0ex]$\Rightarrow$ (st{-}atom(${\it tab}$;$n$) = $x$)
\\[0ex]$\Rightarrow$ \=(($\uparrow$isl(st{-}lookup(${\it tab}$;$x$)))\+
\\[0ex]c$\wedge$ (outl(st{-}lookup(${\it tab}$;$x$)) = $<$key(${\it tab}$;$n$), data(${\it tab}$;$n$)$>$ $\in$ (:($\mathbb{N}$ + Atom1) $\times$ data($T$)))))
\-\-
\end{tabbing}